;; Copyright (c) 2012, 2013 Alan Watson. All rights reserved.

;; BSD-style license: http://synthcode.com/license.txt

(define-library (clock tai-to-utc-offset)

  ;;> \title{Library (clock tai-to-utc-offset)}
  ;;
  ;;> This library implements procedures that give the offset between
  ;;> TAI and UTC at a specified instant.

  (export tai-to-utc-offset-at-utc-day
          tai-to-utc-offset-at-tai-second
          strict-tai-to-utc-offset-at-tai-second)

  (import (scheme base))
  (import (clock leap-seconds))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (include "tai-to-utc-offset-early.scm")

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (begin

    (define seconds-per-day 86400)

    ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

    ;;> \procedure{(tai-to-utc-offset-at-utc-day \var{utc-day})}
    ;;>
    ;;> The \scheme{tai-to-utc-offset-at-utc-day} procedure returns the
    ;;> TAI to UTC offset in SI seconds at the instant specified by its
    ;;> argument \var{utc-day}. The instant is specified by the number of
    ;;> UTC days since 1970-01-01 00:00:00 UTC.
    ;;>
    ;;> The offset will be an inexact real number for instants from
    ;;> 1961-01-01 UTC inclusive to 1972-01-01 UTC exclusive and will be
    ;;> an exact integer for instants after 1972-01-01 UTC inclusive.
    ;;>
    ;;> The procedure signals an error for instants prior to 1961-01-01
    ;;> 00:00:00 UTC exclusive.

    (define (tai-to-utc-offset-at-utc-day utc-day)
      ;; 1972-01-01 UTC corresponds to utc-day 730.
      (if (< utc-day 730)
        (tai-to-utc-offset-at-utc-day-early utc-day)
        (tai-to-utc-offset-at-utc-day-late utc-day)))

    (define (tai-to-utc-offset-at-utc-day-late utc-day)
      (+ 10 (leap-seconds-before-utc-day utc-day)))

    ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

    ;;> \procedure{(tai-to-utc-offset-at-tai-second \var{tai-second})}
    ;;> \procedure{(strict-tai-to-utc-offset-at-tai-second \var{tai-second})}
    ;;>
    ;;> The \scheme{tai-to-utc-offset-at-tai-second} procedure returns TAI
    ;;> to UTC offset in SI seconds at the instant specified by its argument
    ;;> tai-second.  The instant is specified by the number of TAI seconds
    ;;> since 1970-01-01 00:00:00 TAI.
    ;;>
    ;;> The offset will be an inexact real number for instants from
    ;;> 1961-01-01 UTC inclusive to 1972-01-01 UTC exclusive and will be
    ;;> an exact integer for instants after 1972-01-01 UTC inclusive.
    ;;>
    ;;> The procedure signals an error for instants prior to 1961-01-01
    ;;> 00:00:00 UTC (1961-01-01 00:00:01.422818 TAI) exclusive.
    ;;>
    ;;> The \scheme{strict-tai-to-utc-offset-at-tai-second} procedure
    ;;> signals an error if asked for an offset at an instant at which
    ;;> the offset is not defined or is not uniquely defined. The
    ;;> \scheme{tai-to-utc-offset-at-tai-second} procedure extrapolates
    ;;> or gives precedence to earlier equations for the offset, and will
    ;;> always return a value for any instant after 1961-01-01 00:00:00
    ;;> UTC inclusive.

    (define (tai-to-utc-offset-at-tai-second tai-second)
      (if (< tai-second 63072010)
        (tai-to-utc-offset-at-tai-second-early tai-second #f)
        (tai-to-utc-offset-at-tai-second-late tai-second)))

    (define (strict-tai-to-utc-offset-at-tai-second tai-second)
      (if (< tai-second 63072010)
        (tai-to-utc-offset-at-tai-second-early tai-second #t)
        (tai-to-utc-offset-at-tai-second-late tai-second)))

    (define (tai-to-utc-offset-at-tai-second-late tai-second)
      (+ 10 (leap-seconds-before-tai-second tai-second)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;> \section{Notes}
;;>
;;> A useful summary of the history of the TAI and UTC timescales is
;;> given by Seidelmann and Seago (2011, Metrologia, 48, S186,
;;> \url{http://iopscience.iop.org/0026-1394/48/4/S09}).
;;>
;;> \subsection{The Offset from 1972-01-01 UTC onwards}
;;>
;;> Since 1972-01-01 00:00:00 UTC the offset between TAI and UTC has
;;> been defined to 10 seconds plus a variable number of leap seconds.
;;> The number of leap seconds before an instant is obtained from the
;;> \scheme{(clock leap-seconds)} library.
;;>
;;> \subsection{The Offset between 1961-01-01 UTC and 1972-01-01 UTC}
;;>
;;> Between 1961-01-01 UTC inclusive and 1972-01-01 UTC exclusive, the
;;> offset between TAI and UTC is given by a set of linear equations
;;> published by the IERS
;;> (\url{http://hpiers.obspm.fr/iers/bul/bulc/UTC-TAI.history}). These
;;> equations are of the form:
;;>
;;>   TAI - UTC = offset-ref + drift * (mjd - mjd-ref)
;;>
;;> in which mjd is the modified Julian day and offset-ref, drift, and
;;> mjd-ref are constants.
;;>
;;> Each equation is applicable to a specified range of UTC time. At
;;> the end of the range of each equation, the offset is sometimes
;;> continuous, sometimes has an increasing discontinuity, and sometimes
;;> has a decreasing discontinuity.
;;>
;;> The set of equations cover all UTC instants between 1961-01-01
;;> 00:00:00 UTC (inclusive) and 1972-01-01 00:00:00 UTC (exclusive).
;;> Thus, the offset between TAI and UTC is uniquely defined at a given
;;> instant of UTC time
;;>
;;> However, when we attempt to invert the equations, to determine the
;;> offset at a given moment of TAI time, we face two problems related
;;> to the discontinuities.
;;>
;;> When the offset has an increasing discontinuity, there is an
;;> interval of TAI time during which the offset to UTC is formally
;;> not defined.  For example, the offset at the end of 1971-12-31 UTC
;;> is 9.892242 seconds and the offset at the start of 1972-01-01 UTC
;;> is 10 seconds.  Thus, during the interval from 1972-01-01
;;> 00:00:09.892242 TAI to 1972-01-01 00:00:10 TAI, the offset to UTC
;;> is not defined.
;;>
;;> When the offset has a decreasing discontinuity, there is an interval
;;> of TAI time that formally corresponds to two intervals of UTC time.
;;> For example, the offset at the end of 1968-01-31 UTC is 6.285682
;;> and the offset at the start of 1968-02-01 UTC is 6.185682. Thus,
;;> the interval from 1968-02-01 00:00:06.185682 TAI to 1968-02-01
;;> 00:00:06.285682 corresponds an interval of 0.1 seconds just before
;;> to 1968-02-01 00:00:00 UTC and also to an interval of 0.1 seconds
;;> just after 1968-02-01 00:00:00 UTC, and so in this interval of TAI
;;> time the offset to UTC is not uniquely defined.
;;>
;;> One approach to this is to signal an error when asked to calculate
;;> the offset at a moment of TAI time for which the offset is not
;;> defined or for which it is not uniquely defined. This approach is
;;> taken by the \scheme{strict-tai-to-utc-offset-at-tai-second}
;;> procedure.
;;>
;;> Another is to give precedence (when the offset is not uniquely
;;> defined) to or extend the range (when the offset is not defined)
;;> of either the earlier or the later equation. This approach is taken
;;> by the \scheme{tai-to-utc-offset-at-tai-second} procedure. It
;;> extends the earlier equation through periods in which the offset
;;> if not defined and gives precedence to the earlier equation through
;;> periods in which the offset is not uniquely defined.
;;>
;;> \subsection{The Offset Prior to 1961-01-01 UTC}
;;>
;;> The offset between TAI and UTC is not formally defined prior to
;;> 1961-01-01 UTC (although the BIH AM scale and the USNO A.1 scale,
;;> predecessors to TAI, were set to agree with UT2, a predecessor of
;;> UTC, at 1958-01-01 00:00:00).
;;>
;;> Therefore, all of the procedures signal an error when asked for
;;> the offset at an instant prior to 1961-01-01 00:00:00 UTC (1961-01-01
;;> 00:00:01.422818 TAI) exclusive.
;;>
;;> \subsection{Seconds}
;;>
;;> Prior to 1960, the second was defined as 1/86400 of the mean solar
;;> day and was assumed to be constant. In the early 20th century, it
;;> because clear that the mean solar day suffered short-term variations
;;> and a long-term lengthening, and as such was an unsuitable basis
;;> for precise time-keeping.
;;>
;;> From 1960 until 1967, the SI second was defined as equal to a
;;> specified fraction of a specific notional tropical year for 1900,
;;> which mitigated this problem. In 1967, the SI second was redefined
;;> by reference to atomic clocks, but the length of the redefined
;;> second matched that of the previous SI second to 1 part in 10¹⁰
;;> (roughly 3 milliseconds per year). In this work, we assume that
;;> the SI second has been truly constant since 1960.
;;>
;;> The TAI second is by definition equal to the SI second.
;;>
;;> From 1961 to 1972, the UTC second was 1/86400 of the UTC day and
;;> was defined precisely with respect to the SI second. At various
;;> points, it was longer than the SI second by 130, 150, and 300 SI
;;> nanoseconds. From 1972-01-01, the UTC second has been defined to
;;> be equal to the SI second.
